feat: Allow forall statements in statement expressions #5894

RustanLeino · 2024-11-04T01:31:34Z

This PR adds forall statements to the statements supported in StmtExprs. Previously, one had to write

assert forall x | R(x) :: P(x) by {
  forall x | R(x)
    ensures P(x)
  {
    // proof that R(x) ==> P(x)
  }
}
ExprBody

as an expression. Now, one can simply write

forall x | R(x)
  ensures P(x)
{
  // proof that R(x) ==> P(x)
}
ExprBody

The PR also deprecates the ancient syntax where parentheses enclosing the bound variables in the forall statement.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

MikaelMayer

Two minor issues. Overall good implementation.

MikaelMayer · 2024-11-07T13:25:31Z

Source/DafnyCore/Dafny.atg

-  .)
+  QuantifierDomain<out bvars, out attrs, out range, true, true, true>
+  ( IF(univ && (la.kind == _ensures || la.kind == _lbrace))
+    // It's a forall statement. Parse it as part of a StmtExpr.


That works. It means we could theoretically do the same for if statements (last week I would have loved to have that) and I think that could be useful too and less surprising in the future, although out of scope for this PR.

I agree it's out of scope for this PR, but I do find it an interesting idea. I suppose such an if statement would still just be for the StmtExpr, rather than being an alternative syntax for if-then-else expressions? This would then allow you to write some proofs inside the if statement and follow that by the expression you want to return. (I have never felt the need for this myself, but perhaps only because I knew the feature wasn't available.)

Some new users confuse if-then-else expressions and if statements (which, curiously, seems not to be a confusion in languages that use the more cryptic ? : for the former). On one hand, also allowing if statements in expressions might add to that confusion. But on the other hand, maybe this would give us a place in the parser to give a better error message if the program gets this wrong.

While we're thinking about such things, one could also imagine other statements, in particular while loops, in expressions. Again, such a while statement would just be for the StmtExpr, to allow an inline proof that uses a loop.

MikaelMayer · 2024-11-07T13:30:01Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Parallel.dfy.expect

@@ -1,3 +1,4 @@
+Parallel.dfy(267,11): Warning: parentheses around the forall-statement bound variables are deprecated and not needed


I'd rather remove the parentheses on our test suite. LLMs are going to learn from it :-)
To test the warning message, prefer a dedicated file that includes deprecated in its name and make sure to put as a comment where you expect the warning

Okay, I'll remove them from this place, too. (I had kept them in one place in order to test the warning message, but I agree with you that we're better served by not teaching LLMs out there deprecated syntax.)

Here's what I did, following your remark: I moved the forall-statement deprecation tests to dafny0/Deprecation.dfy (and added some more such tests). And I added comments on the lines in the test file to indicate where we expect error messages.

I also renamed the Parallel*.dfy tests ForallStmt*.dfy. (Originally, the forall statement had been named foreach. But that suggests a sequential ordering. So, the statement was renamed parallel. This confused people, so (years ago) the statement was once again renamed to the current forall.)

keyboardDrummer · 2024-11-12T11:44:36Z

IMO the way Dafny defines expressions and statement is unnecessarily confusing and we should resolve that. Many concepts occur both in the expression and the statement space, but either behave or appear slightly differently, and then some things that behave like statements are also available in expressions using "statement expressions", which I've never seen before in a language and IMO goes against the concept of an expression: that execution order is not relevant to its semantics.

I think part of the solution is to merge Dafny functions and methods: allowing methods to be called where currently only functions can be, removing the need for functions. This requires proving that the method is pure, that it has no side-effects and behaves deterministically, which is something we currently do not support, but I think it would be a great improvement.

I'm hopeful this would allow removing statement expressions, even though they could still be useful in contracts to prove preconditions of calls that occur in them.

I'm not a big fan of var expressions, since they look like variables while they do not behave like them: they're not reassignable. I also think the order is incorrect: when working with expressions the declarations should be specified top down, the top-level expression first, and the subexpressions later, similar to how where in Haskell works.

For if statements and expressions, I think the problem is that the keywords are the same but the syntax is different. Either we should unify the syntax, or introduce separate keywords/operators.

In conclusion, I would rather have us focus our efforts on removing the need for statements expressions, than expanding what's possible with them.

RustanLeino · 2024-11-13T01:43:39Z

@keyboardDrummer I disagree on many accounts.

It's not surprising that you haven't seen statement expressions in other languages, since their only purpose is to introduce information to the verifier. Dafny also has by clauses and witness clauses, which give information to the verifier, and these do not exist in languages that are not focused on verification.

Dafny has a clean separation between expressions and statements. This lets the language distinguish between effectful things and "pure" things. It is difficult to achieve such a separation in a language that only has, say, methods -- for example, in Java, it is difficult to define what a "pure method" would be, with a definition that allows the method to be used in expressions suitable for the verifier. Merging expressions and statements in Dafny would only make Dafny unsuitable for verification.

Note that the statements that are allowed in statement expressions are like lemmas in that they don't change the program state.

Do you have a suggestion for a new keyword for either if statements or if-then-else expressions?

Variables are introduced with the var keyword. But those variables introduced in an expression are not mutable.

Back to the forall statement. There is sometimes a need to introduce universally quantified information for the verifier. Today, that can be done in expressions only by the clumsy assert forall ... by { forall ... { ... } } construction shown in the description of this PR. The only reason forall statements were not among the statements allowed in a statement expression before was that they appeared to introduce parsing problems. As this PR demonstrates, it is not difficult to change the grammar to distinguish between forall expressions and forall statements. Hence, the feature introduced by this PR is a win for the customer, and I think it rather makes the language more consistent rather than polluting it with another feature.

keyboardDrummer · 2024-11-13T11:18:46Z

it is difficult to define what a "pure method" would be, with a definition that allows the method to be used in expressions suitable for the verifier

What's missing in the definition I provided? The method may not modify any state (modifies {}) and must be deterministic, (any two invocations with equal parameters (including heap) return an equal result, using Dafny's existing definition of equality)

Back to the forall statement.
...

I agree that given the existence of statement expressions, it is better if forall statements are included in those. However, whether it's a good investment to add them hinges on whether we want to keep statement expressions.

Do you have a suggestion for a new keyword for either if statements or if-then-else expressions?

If we don't unify the syntax, then I think using ternary operators (? :) for the expression version would be better than how it is now.

However, I think ideally it would be a single syntax for both expressions and statements. There was a discussion in this ticket #2899 and it would probably be best to continue there. I still like @MikaelMayer 's proposal there.

Variables are introduced with the var keyword. But those variables introduced in an expression are not mutable.

I'd discuss more but it'd be better to use a separate GH issue for that. My bad for mentioning it here in the first place. Created an issue: #5914

RustanLeino · 2024-11-14T18:55:27Z

While those things are being discussed elsewhere, can we move forward with accepting this PR? @MikaelMayer @keyboardDrummer

RustanLeino added 6 commits November 3, 2024 16:51

Improve code and comments

31f2136

Make test run with both resolvers

414c4c1

Allow forall statements in statement expressions

6f97e14

Deprecate forall statements with parenthesized bound variables

216b63a

Update documentation

2921cd4

Add release notes

fd7ea46

RustanLeino marked this pull request as ready for review November 4, 2024 01:32

RustanLeino enabled auto-merge (squash) November 4, 2024 01:32

RustanLeino added 3 commits November 3, 2024 18:12

Fix deprecated parentheses in standard library

ace95ab

Adjust tests

463a5f6

Merge branch 'master' into forall-stmt-in-expr

137f3ad

MikaelMayer reviewed Nov 7, 2024

View reviewed changes

RustanLeino added 4 commits November 7, 2024 09:57

Merge branch 'master' into forall-stmt-in-expr

2e60809

Move deprecation tests to Deprecation.dfy

1ede1ce

Rename Parallel* test files to ForallStmt*

e191c36

Applying renaming in test files

1dbad1b

Merge branch 'master' into forall-stmt-in-expr

81ca722

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: Allow forall statements in statement expressions #5894

feat: Allow forall statements in statement expressions #5894

RustanLeino commented Nov 4, 2024 •

edited

Loading

MikaelMayer left a comment

MikaelMayer Nov 7, 2024 •

edited

Loading

RustanLeino Nov 7, 2024

MikaelMayer Nov 7, 2024

RustanLeino Nov 7, 2024

RustanLeino Nov 7, 2024

keyboardDrummer commented Nov 12, 2024 •

edited

Loading

RustanLeino commented Nov 13, 2024

keyboardDrummer commented Nov 13, 2024 •

edited

Loading

RustanLeino commented Nov 14, 2024

		@@ -1,3 +1,4 @@
		Parallel.dfy(267,11): Warning: parentheses around the forall-statement bound variables are deprecated and not needed

feat: Allow forall statements in statement expressions #5894

Are you sure you want to change the base?

feat: Allow forall statements in statement expressions #5894

Conversation

RustanLeino commented Nov 4, 2024 • edited Loading

MikaelMayer left a comment

Choose a reason for hiding this comment

MikaelMayer Nov 7, 2024 • edited Loading

Choose a reason for hiding this comment

RustanLeino Nov 7, 2024

Choose a reason for hiding this comment

MikaelMayer Nov 7, 2024

Choose a reason for hiding this comment

RustanLeino Nov 7, 2024

Choose a reason for hiding this comment

RustanLeino Nov 7, 2024

Choose a reason for hiding this comment

keyboardDrummer commented Nov 12, 2024 • edited Loading

RustanLeino commented Nov 13, 2024

keyboardDrummer commented Nov 13, 2024 • edited Loading

RustanLeino commented Nov 14, 2024

RustanLeino commented Nov 4, 2024 •

edited

Loading

MikaelMayer Nov 7, 2024 •

edited

Loading

keyboardDrummer commented Nov 12, 2024 •

edited

Loading

keyboardDrummer commented Nov 13, 2024 •

edited

Loading